/*
 *      Copyright (c) 2023 by Hex-Rays, support@hex-rays.com
 *      ALL RIGHTS RESERVED.
 *
 *      gooMBA plugin for Hex-Rays Decompiler.
 *
 */

#include "z3++_no_warn.h"
#include "bitwise_expr_lookup_tbl.hpp"

bw_expr_tbl_t bw_expr_tbl_t::instance;

bw_expr_tbl_t::bw_expr_tbl_t()
{
  minsn_templates_t X;
  X.push_back(std::make_shared<mt_varref_t>(0));
  X.push_back(std::make_shared<mt_varref_t>(1));
  X.push_back(std::make_shared<mt_varref_t>(2));

  minsn_template_ptr_t zero = std::make_shared<mt_constant_t>(0ull);

  // note that all expressions are ordered by the numeric value of the instruction trace
  // see lin_conj_exprs.hpp for more info on ordering.
  auto &onevar = tbl.push_back();
  onevar.push_back(zero); // [0 0]
  onevar.push_back(X[0]); // [0 1]

  auto &twovar = tbl.push_back();
  twovar.push_back(zero);           // [0 0 0 0]
  twovar.push_back(X[0]&~X[1]);     // [0 1 0 0]
  twovar.push_back(~(X[0]|~X[1]));  // [0 0 1 0]
  twovar.push_back(X[0]^X[1]);      // [0 1 1 0]
  twovar.push_back(X[0]&X[1]);      // [0 0 0 1]
  twovar.push_back(X[0]);           // [0 1 0 1]
  twovar.push_back(X[1]);           // [0 0 1 1]
  twovar.push_back(X[0]|X[1]);      // [0 1 1 1]

  auto &threevar = tbl.push_back();
  threevar.push_back(zero);                                   // [0 0 0 0 0 0 0 0]
  threevar.push_back(~(~X[0]|(X[1]|X[2])));                   // [0 1 0 0 0 0 0 0]
  threevar.push_back(~(X[0]|(~X[1]|X[2])));                   // [0 0 1 0 0 0 0 0]
  threevar.push_back(~X[2]&(X[0]^X[1]));                      // [0 1 1 0 0 0 0 0]
  threevar.push_back(~(~X[0]|(~X[1]|X[2])));                  // [0 0 0 1 0 0 0 0]
  threevar.push_back(X[0]&~X[2]);                             // [0 1 0 1 0 0 0 0]
  threevar.push_back(X[1]&~X[2]);                             // [0 0 1 1 0 0 0 0]
  threevar.push_back(X[2]^(X[0]|(X[1]|X[2])));                // [0 1 1 1 0 0 0 0]
  threevar.push_back(~X[0]&(~X[1]&X[2]));                     // [0 0 0 0 1 0 0 0]
  threevar.push_back(~X[1]&(X[0]^X[2]));                      // [0 1 0 0 1 0 0 0]
  threevar.push_back(~X[0]&(X[1]^X[2]));                      // [0 0 1 0 1 0 0 0]
  threevar.push_back(~(X[0]&X[1])&(X[0]^(X[1]^X[2])));        // [0 1 1 0 1 0 0 0]
  threevar.push_back(~(X[0]^X[1])&(X[0]^X[2]));               // [0 0 0 1 1 0 0 0]
  threevar.push_back(X[2]^(X[0]|(X[1]&X[2])));                // [0 1 0 1 1 0 0 0]
  threevar.push_back(~(X[0]&~X[1])&(X[1]^X[2]));              // [0 0 1 1 1 0 0 0]
  threevar.push_back(X[2]^(X[0]|X[1]));                       // [0 1 1 1 1 0 0 0]
  threevar.push_back(X[0]&(~X[1]&X[2]));                      // [0 0 0 0 0 1 0 0]
  threevar.push_back(X[0]&~X[1]);                             // [0 1 0 0 0 1 0 0]
  threevar.push_back((X[0]^X[1])&~(X[0]^X[2]));               // [0 0 1 0 0 1 0 0]
  threevar.push_back(X[1]^(X[0]|(X[1]&X[2])));                // [0 1 1 0 0 1 0 0]
  threevar.push_back(X[0]&(X[1]^X[2]));                       // [0 0 0 1 0 1 0 0]
  threevar.push_back(~(~X[0]|(X[1]&X[2])));                   // [0 1 0 1 0 1 0 0]
  threevar.push_back((X[0]|X[1])&(X[1]^X[2]));                // [0 0 1 1 0 1 0 0]
  threevar.push_back((X[0]&X[1])^~(X[0]^(~X[1]|X[2])));       // [0 1 1 1 0 1 0 0]
  threevar.push_back(~(X[1]|~X[2]));                          // [0 0 0 0 1 1 0 0]
  threevar.push_back(X[1]^(X[0]|(X[1]|X[2])));                // [0 1 0 0 1 1 0 0]
  threevar.push_back(~(X[0]&X[1])&(X[1]^X[2]));               // [0 0 1 0 1 1 0 0]
  threevar.push_back(X[1]^(X[0]|X[2]));                       // [0 1 1 0 1 1 0 0]
  threevar.push_back((X[0]|~X[1])&(X[1]^X[2]));               // [0 0 0 1 1 1 0 0]
  threevar.push_back((X[0]&X[2])^(X[0]^(~X[1]&X[2])));        // [0 1 0 1 1 1 0 0]
  threevar.push_back(X[1]^X[2]);                              // [0 0 1 1 1 1 0 0]
  threevar.push_back((X[0]&~X[1])|(X[1]^X[2]));               // [0 1 1 1 1 1 0 0]
  threevar.push_back(~X[0]&(X[1]&X[2]));                      // [0 0 0 0 0 0 1 0]
  threevar.push_back((X[0]^X[1])&(X[0]^X[2]));                // [0 1 0 0 0 0 1 0]
  threevar.push_back(~(X[0]|~X[1]));                          // [0 0 1 0 0 0 1 0]
  threevar.push_back(X[1]^~(~X[0]|(~X[1]&X[2])));             // [0 1 1 0 0 0 1 0]
  threevar.push_back(X[1]&(X[0]^X[2]));                       // [0 0 0 1 0 0 1 0]
  threevar.push_back(X[2]^(X[0]|(~X[1]&X[2])));               // [0 1 0 1 0 0 1 0]
  threevar.push_back(X[1]&~(X[0]&X[2]));                      // [0 0 1 1 0 0 1 0]
  threevar.push_back(X[1]^~(~X[0]|(X[1]^X[2])));              // [0 1 1 1 0 0 1 0]
  threevar.push_back(~(X[0]|~X[2]));                          // [0 0 0 0 1 0 1 0]
  threevar.push_back(X[2]^(X[0]&(~X[1]|X[2])));               // [0 1 0 0 1 0 1 0]
  threevar.push_back(~X[0]&(X[1]|X[2]));                      // [0 0 1 0 1 0 1 0]
  threevar.push_back(X[0]^(X[1]|X[2]));                       // [0 1 1 0 1 0 1 0]
  threevar.push_back(X[2]^(X[0]&(X[1]|X[2])));                // [0 0 0 1 1 0 1 0]
  threevar.push_back(X[0]^X[2]);                              // [0 1 0 1 1 0 1 0]
  threevar.push_back((X[0]&X[2])^(X[1]|X[2]));                // [0 0 1 1 1 0 1 0]
  threevar.push_back(X[2]^~(~X[0]&(~X[1]|X[2])));             // [0 1 1 1 1 0 1 0]
  threevar.push_back(X[2]&(X[0]^X[1]));                       // [0 0 0 0 0 1 1 0]
  threevar.push_back(X[1]^~(~X[0]&(~X[1]|X[2])));             // [0 1 0 0 0 1 1 0]
  threevar.push_back(X[1]^(X[0]&(X[1]|X[2])));                // [0 0 1 0 0 1 1 0]
  threevar.push_back(X[0]^X[1]);                              // [0 1 1 0 0 1 1 0]
  threevar.push_back((X[0]|X[1])&~(X[0]^(X[1]^X[2])));        // [0 0 0 1 0 1 1 0]
  threevar.push_back(X[0]^(X[1]&X[2]));                       // [0 1 0 1 0 1 1 0]
  threevar.push_back(X[1]^(X[0]&X[2]));                       // [0 0 1 1 0 1 1 0]
  threevar.push_back(X[1]^(X[0]&(~X[1]|X[2])));               // [0 1 1 1 0 1 1 0]
  threevar.push_back(X[2]&~(X[0]&X[1]));                      // [0 0 0 0 1 1 1 0]
  threevar.push_back(X[1]^(X[0]|(X[1]^X[2])));                // [0 1 0 0 1 1 1 0]
  threevar.push_back((X[0]&X[1])^(X[1]|X[2]));                // [0 0 1 0 1 1 1 0]
  threevar.push_back(X[1]^(X[0]|(~X[1]&X[2])));               // [0 1 1 0 1 1 1 0]
  threevar.push_back(X[2]^(X[0]&X[1]));                       // [0 0 0 1 1 1 1 0]
  threevar.push_back(X[2]^~(~X[0]|(~X[1]&X[2])));             // [0 1 0 1 1 1 1 0]
  threevar.push_back(~(X[0]|~X[1])|(X[1]^X[2]));              // [0 0 1 1 1 1 1 0]
  threevar.push_back((X[0]^X[1])|(X[0]^X[2]));                // [0 1 1 1 1 1 1 0]
  threevar.push_back(X[0]&(X[1]&X[2]));                       // [0 0 0 0 0 0 0 1]
  threevar.push_back(~(~X[0]|(X[1]^X[2])));                   // [0 1 0 0 0 0 0 1]
  threevar.push_back(X[1]&~(X[0]^X[2]));                      // [0 0 1 0 0 0 0 1]
  threevar.push_back((X[0]|X[1])&(X[0]^(X[1]^X[2])));         // [0 1 1 0 0 0 0 1]
  threevar.push_back(X[0]&X[1]);                              // [0 0 0 1 0 0 0 1]
  threevar.push_back(~(~X[0]|(~X[1]&X[2])));                  // [0 1 0 1 0 0 0 1]
  threevar.push_back(X[1]&(X[0]|~X[2]));                      // [0 0 1 1 0 0 0 1]
  threevar.push_back((X[1]&~X[2])|~(~X[0]|(~X[1]&X[2])));     // [0 1 1 1 0 0 0 1]
  threevar.push_back(X[2]&~(X[0]^X[1]));                      // [0 0 0 0 1 0 0 1]
  threevar.push_back((X[0]|~X[1])&(X[0]^(X[1]^X[2])));        // [0 1 0 0 1 0 0 1]
  threevar.push_back(~(X[0]&~X[1])&(X[0]^(X[1]^X[2])));       // [0 0 1 0 1 0 0 1]
  threevar.push_back(X[0]^(X[1]^X[2]));                       // [0 1 1 0 1 0 0 1]
  threevar.push_back(X[1]^(~X[0]&(X[1]|X[2])));               // [0 0 0 1 1 0 0 1]
  threevar.push_back(X[0]^(~X[1]&X[2]));                      // [0 1 0 1 1 0 0 1]
  threevar.push_back(X[1]^~(X[0]|~X[2]));                     // [0 0 1 1 1 0 0 1]
  threevar.push_back((X[0]&X[1])|(X[0]^(X[1]^X[2])));         // [0 1 1 1 1 0 0 1]
  threevar.push_back(X[0]&X[2]);                              // [0 0 0 0 0 1 0 1]
  threevar.push_back(X[0]&(~X[1]|X[2]));                      // [0 1 0 0 0 1 0 1]
  threevar.push_back(X[2]^(~X[0]&(X[1]|X[2])));               // [0 0 1 0 0 1 0 1]
  threevar.push_back(~(X[0]^(~X[1]|X[2])));                   // [0 1 1 0 0 1 0 1]
  threevar.push_back(X[0]&(X[1]|X[2]));                       // [0 0 0 1 0 1 0 1]
  threevar.push_back(X[0]);                                   // [0 1 0 1 0 1 0 1]
  threevar.push_back((X[0]&X[2])|(X[1]&~X[2]));               // [0 0 1 1 0 1 0 1]
  threevar.push_back(~(~X[0]&(~X[1]|X[2])));                  // [0 1 1 1 0 1 0 1]
  threevar.push_back(X[2]&(X[0]|~X[1]));                      // [0 0 0 0 1 1 0 1]
  threevar.push_back((X[1]&~X[2])^(X[0]|(X[1]^X[2])));        // [0 1 0 0 1 1 0 1]
  threevar.push_back(X[2]^~(X[0]|~X[1]));                     // [0 0 1 0 1 1 0 1]
  threevar.push_back((X[0]&~X[1])|(X[0]^(X[1]^X[2])));        // [0 1 1 0 1 1 0 1]
  threevar.push_back((X[0]&X[1])|~(X[1]|~X[2]));              // [0 0 0 1 1 1 0 1]
  threevar.push_back(X[0]|(~X[1]&X[2]));                      // [0 1 0 1 1 1 0 1]
  threevar.push_back((X[0]&X[1])|(X[1]^X[2]));                // [0 0 1 1 1 1 0 1]
  threevar.push_back(X[0]|(X[1]^X[2]));                       // [0 1 1 1 1 1 0 1]
  threevar.push_back(X[1]&X[2]);                              // [0 0 0 0 0 0 1 1]
  threevar.push_back((X[0]|X[1])&~(X[1]^X[2]));               // [0 1 0 0 0 0 1 1]
  threevar.push_back(X[1]&~(X[0]&~X[2]));                     // [0 0 1 0 0 0 1 1]
  threevar.push_back(X[1]^(X[0]&~X[2]));                      // [0 1 1 0 0 0 1 1]
  threevar.push_back(X[1]&(X[0]|X[2]));                       // [0 0 0 1 0 0 1 1]
  threevar.push_back((X[0]&X[2])^(X[0]^(X[1]&X[2])));         // [0 1 0 1 0 0 1 1]
  threevar.push_back(X[1]);                                   // [0 0 1 1 0 0 1 1]
  threevar.push_back(X[1]|(X[0]&~X[2]));                      // [0 1 1 1 0 0 1 1]
  threevar.push_back(X[2]&~(X[0]&~X[1]));                     // [0 0 0 0 1 0 1 1]
  threevar.push_back(X[2]^(X[0]&~X[1]));                      // [0 1 0 0 1 0 1 1]
  threevar.push_back((X[1]&X[2])|(~X[0]&(X[1]|X[2])));        // [0 0 1 0 1 0 1 1]
  threevar.push_back(~(X[0]|~X[1])|(X[0]^(X[1]^X[2])));       // [0 1 1 0 1 0 1 1]
  threevar.push_back(X[1]^(~X[0]&(X[1]^X[2])));               // [0 0 0 1 1 0 1 1]
  threevar.push_back(X[2]^~(~X[0]|(X[1]&X[2])));              // [0 1 0 1 1 0 1 1]
  threevar.push_back(X[1]|~(X[0]|~X[2]));                     // [0 0 1 1 1 0 1 1]
  threevar.push_back(X[1]|(X[0]^X[2]));                       // [0 1 1 1 1 0 1 1]
  threevar.push_back(X[2]&(X[0]|X[1]));                       // [0 0 0 0 0 1 1 1]
  threevar.push_back((X[0]&X[1])^(X[0]^(X[1]&X[2])));         // [0 1 0 0 0 1 1 1]
  threevar.push_back(X[1]^(X[0]&(X[1]^X[2])));                // [0 0 1 0 0 1 1 1]
  threevar.push_back(X[1]^~(~X[0]|(X[1]&X[2])));              // [0 1 1 0 0 1 1 1]
  threevar.push_back((X[1]&X[2])|(X[0]&(X[1]|X[2])));         // [0 0 0 1 0 1 1 1]
  threevar.push_back(X[0]|(X[1]&X[2]));                       // [0 1 0 1 0 1 1 1]
  threevar.push_back(X[1]|(X[0]&X[2]));                       // [0 0 1 1 0 1 1 1]
  threevar.push_back(X[0]|X[1]);                              // [0 1 1 1 0 1 1 1]
  threevar.push_back(X[2]);                                   // [0 0 0 0 1 1 1 1]
  threevar.push_back(X[2]|(X[0]&~X[1]));                      // [0 1 0 0 1 1 1 1]
  threevar.push_back(X[2]|~(X[0]|~X[1]));                     // [0 0 1 0 1 1 1 1]
  threevar.push_back(X[2]|(X[0]^X[1]));                       // [0 1 1 0 1 1 1 1]
  threevar.push_back(X[2]|(X[0]&X[1]));                       // [0 0 0 1 1 1 1 1]
  threevar.push_back(X[0]|X[2]);                              // [0 1 0 1 1 1 1 1]
  threevar.push_back(X[1]|X[2]);                              // [0 0 1 1 1 1 1 1]
  threevar.push_back(X[0]|(X[1]|X[2]));                       // [0 1 1 1 1 1 1 1]
}
